using Microsoft.VisualStudio.TestTools.UnitTesting;

using System.Collections.Generic;

namespace Weazel.Gezel.Model.Test
{
  using Mod = Weazel.Gezel.Model;    
  using Weazel.Gezel.Parser;
  using Weazel.Gezel.Model.Errors;

  [TestClass]
  public class TestControllerVerification
  {
    [TestMethod]
    public void TestUnknownDatapath()
    {
      List<ParseError> parseErrors = new List<ParseError>();
			List<VerificationError> verificationErrors = new List<VerificationError>();
			List<VerificationWarning> warnings = new List<VerificationWarning>();

      Model model = ParseModel.Parse(ref parseErrors, "hardwired test_hw(my_nonexistent_dp) { foo; }");

      model.Verify(ref verificationErrors, ref warnings);

      Assert.AreEqual(verificationErrors.Count, 1);
      Assert.AreEqual(verificationErrors[0].ErrorType, VerificationErrorType.ControllerUnknownDatapath);
    }

    [TestMethod]
    public void TestMissingInitialState()
    {
      const string desc = "dp mydp { sfg foo { } }              "+ 
                    "fsm test_fsm(mydp) { state s0, s1; @s0 (foo) -> s1;   } ";

      List<ParseError> parseErrors = new List<ParseError>();
			List<VerificationError> verificationErrors = null;
			List<VerificationWarning> warnings = null;

      Model model = ParseModel.Parse(ref parseErrors, desc);

      Assert.AreEqual(0, parseErrors.Count);

      model.Verify(ref verificationErrors, ref warnings);

			Assert.AreEqual(1, verificationErrors.Count);
			Assert.AreEqual(VerificationErrorType.ControllerNoInitialState, verificationErrors[0].ErrorType);
    }

    [TestMethod]
    public void TestUnknownSignalFlowGraphName()
    {
      List<ParseError> parseErrors = new List<ParseError>();
			List<VerificationError> verificationErrors = null;
			List<VerificationWarning> warnings = null;

      const string description =
        "dp mydp { sfg run {} }" +
        "hardwired ctrl(mydp) { wrong; }";

      Model model = ParseModel.Parse(ref parseErrors, description);

      foreach (ParseError e in parseErrors)
        System.Windows.Forms.MessageBox.Show(e.ToString());

      Assert.AreEqual(0, parseErrors.Count);

      model.Verify(ref verificationErrors, ref warnings);

      Assert.AreEqual(1, verificationErrors.Count);
      Assert.AreEqual(VerificationErrorType.ControllerNoSfg, verificationErrors[0].ErrorType);
    }

    [TestMethod]
    public void TestUndeclaredSourceState()
    {
      List<ParseError> parseErrors = new List<ParseError>();
			List<VerificationError> verificationErrors = null;
			List<VerificationWarning> warnings = null;

      const string description =
        "dp pede { sfg exec { } } " +
        "fsm frede(pede) { initial s2; @s1 (exec) -> s2; } ";

      Model model = ParseModel.Parse(ref parseErrors, description);

      Assert.AreEqual(0, parseErrors.Count);

      model.Verify(ref verificationErrors, ref warnings);

      Assert.AreEqual(1, verificationErrors.Count);
      Assert.AreEqual(VerificationErrorType.ControllerUndeclaredSourceState, verificationErrors[0].ErrorType);
    }

    [TestMethod]
    public void TestNoTransitionsInFsmController()
    {
      List<ParseError> parseErrors = new List<ParseError>();
			List<VerificationError> verificationErrors = null;
			List<VerificationWarning> warnings = null;

      const string description =
        "dp mydp { sfg exec {} } " +
        "fsm ctrl(mydp) { initial s0; } ";

      Model model = ParseModel.Parse(ref parseErrors, description);

      Assert.AreEqual(0, parseErrors.Count);

      model.Verify(ref verificationErrors, ref warnings);

      Assert.AreEqual(1, verificationErrors.Count);
      Assert.AreEqual(VerificationErrorType.ControllerFsmNoTransitions, verificationErrors[0].ErrorType);
    }

    [TestMethod]
    public void TestTransitionConditionError()
    {
      List<ParseError> parseErrors = new List<ParseError>();
			List<VerificationError> verificationErrors = null;
			List<VerificationWarning> warnings = null;

      const string description =
        " dp mydp {                                 " +
        "   sfg exec { }                            " +
        " }                                         " +
        " fsm ctrl(mydp) {                          " +
        "   initial s0;                             " +
        "   state s1, s2;                           " +
        "   @s0 if(a) then                          " +
        "				  if(b) then (exec) -> s1;          " +
        "	 				else (exec) -> s1;                " +
        "       else (exec) -> s2;                  " +
        " }                                         ";

      Model model = ParseModel.Parse(ref parseErrors, description);

      Assert.AreEqual(0, parseErrors.Count);

      model.Verify(ref verificationErrors, ref warnings);

      Assert.AreEqual(2, verificationErrors.Count);
      Assert.AreEqual(VerificationErrorType.ExpressionInvalidIdentifier, verificationErrors[0].ErrorType);
      Assert.AreEqual(VerificationErrorType.ExpressionInvalidIdentifier, verificationErrors[1].ErrorType);
    }

    [TestMethod]
    public void TestMultipleTracersWithSameDestinationFile()
    {
      List<ParseError> parseErrors = new List<ParseError>();
			List<VerificationError> verificationErrors = null;
			List<VerificationWarning> warnings = null;

      const string description =
        "dp myblock(in a: ns(8)) { " +
        " $trace(a, \"a.txt\"); " + 
        " $trace(-a, \"a.txt\"); " +
        " sfg exec {} } " +
        " hardwired h(myblock) { exec; } " +
        "system T { } ";

      Model model = ParseModel.Parse(ref parseErrors, description);

      Assert.AreEqual(0, parseErrors.Count);

      model.Verify(ref verificationErrors, ref warnings);

      Assert.AreEqual(1, verificationErrors.Count);
      Assert.AreEqual(VerificationErrorType.MultipleUsesOfTracerFile,
        verificationErrors[0].ErrorType);
    }
  }
}